Kind{-}deq
\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$union{-}deq((:IdLnk $\times$ Id); Id; product{-}deq(IdLnk; Id; idlnk{-}deq; id{-}deq); id{-}deq)